Skip to content

feat: add Martinet totally-real towers eval problem#388

Closed
adamtopaz wants to merge 3 commits into
leanprover:mainfrom
mathlib-initiative:add-martinet-totally-real-towers
Closed

feat: add Martinet totally-real towers eval problem#388
adamtopaz wants to merge 3 commits into
leanprover:mainfrom
mathlib-initiative:add-martinet-totally-real-towers

Conversation

@adamtopaz
Copy link
Copy Markdown

Adds Martinet's bounded-root-discriminant theorem for totally real class-field towers. This is used in https://arxiv.org/abs/2605.28781 (see Theorem 3.2).

This PR was prepared with the help of Codex.

@adamtopaz
Copy link
Copy Markdown
Author

Closing since this duplicates #385

@adamtopaz adamtopaz closed this Jun 3, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant